$\forall$$A$:Type, $B$:($A$$\rightarrow$Type), ${\it eq}$:EqDecider($A$), $x$:$A$, $y$:$B$($x$), $a$:Atom1.
\\[0ex]AtomFree(Type;$A$)
\\[0ex]$\Rightarrow$ AtomFree($A$$\rightarrow$Type;$B$)
\\[0ex]$\Rightarrow$ ($\forall$$x$:$A$. AtomFree($A$;$x$))
\\[0ex]$\Rightarrow$ AtomFree(EqDecider($A$);${\it eq}$)
\\[0ex]$\Rightarrow$ $y$:$B$($x$)$>>$$a$
\\[0ex]$\Rightarrow$ $\langle$$x$$,\,$$y$$\rangle$:$x$:$A$$\times$$B$($x$)$>>$$a$